% !Mode:: "TeX:UTF-8"
\chapter*{Заключение}
\addcontentsline{toc}{chapter}{Заключение}

Основные научные и практические результаты, полученные в
диссертационной работе и выносимые на защиту, состоят в следующем:

\begin{enumerate}
    \item предложен подход к построению тестовых программ для проверки подсистем управления памяти микропроцессоров на основе построения и решения систем ограничений;

    \item предложены модель блоков памяти, описывающая его структурные и функциональные характеристики, и модель инструкций, описывающая отдельные пути их выполнения в виде утверждений о свойствах параметров инструкций и свойств наличия или отсутствия данных в блоках;

    \item в рамках предложенного подхода разработаны и формально обоснованы методы построения ограничений, выражающих с использованием битовых операций свойства наличия или отсутствия данных в блоках памяти; свойства вытеснения;

    \item создан прототип системы построения тестовых программ для проверки подсистем управления памяти и проведены эксперименты, показывающие эффективность разработанных методов.
\end{enumerate}

Основные результаты диссертации являются новыми, получены автором самостоятельно.

%\begin{itemize}
  %\item Разработан метод генерации ограничений для тестовых
%шаблонов, нацеленных на тестирование инструкций обращения к памяти,
%с использованием заданного начального состояния микропроцессора,
%который использует свойство инструкций изменять состояния нескольких
%кэширующих буферов (\emph{совместная генерация ограничений}). Метод
%параметризован методом записи стратегии вытеснения в виде
%ограничений. Доказана корректность метода для любых тестовых
%шаблонов и полнота при некоторых дополнительных условиях на тестовые
%шаблоны. Метод позволяет эффективно строить тестовые программы по
%тестовым шаблонам, перед исполнением которых не меняется состояние
%кэширующих буферов микропроцессора.
%
  %\item Разработан метод генерации ограничений для тестовых
%шаблонов, нацеленных на тестирование инструкций обращения к памяти,
%без использования начального состояния микропроцессора
%(\emph{зеркальная генерация ограничений}). Метод параметризован
%методом записи стратегии вытеснения в виде ограничений. Доказана
%корректность метода для любых тестовых шаблонов и полнота при
%некоторых дополнительных условиях на стратегии вытеснения. Показано,
%что наиболее часто используемые в микропроцессорах стратегии
%вытеснения удовлетворяют этим дополнительным условиям, что
%обеспечивает полноту зеркального метода генерации ограничений в
%практически значимых случаях. Отсутствие требования предъявить
%начальное состояние микропроцессора позволяет упростить процесс
%тестирования, поскольку перед построением очередной тестовой
%программы не нужно считывать текущее состояние микропроцессора. Тем
%самым пакет тестовых программ может быть построен полностью до
%проведения тестирования.
%
  %\item Разработан метод генерации ограничений для описания
  %стратегий вытеснения перебором частей тестовой программы,
  %непосредственно влияющих на вытеснение (\emph{перебор диапазонов
  %вытеснения}). Приведены ограничения, генерируемые этим методом,
  %для стратегий вытеснения \LRU, \FIFO и \PseudoLRU, наиболее
  %используемых стратегий вытеснения в микропроцессорах. Показана
  %эквивалентность этих ограничений определениям стратегий
  %вытеснения. Метод может быть эффективно использован в случае
  %кэширующих буферов небольшого размера, каковыми являются,
  %например, буферы трансляции адресов некоторых микропроцессоров.
%
  %\item Разработан метод генерации ограничений для описания
  %стратегий вытеснения, представляющий условие вытеснение в виде
  %границы (верхней или нижней) на количество инструкций,
  %непосредственно влияющих на вытеснение (\emph{метод функций
  %полезности}). Приведены ограничения, генерируемые этим методом,
  %для стратегий вытеснения \LRU, \FIFO и \PseudoLRU, наиболее
  %используемых стратегий вытеснения в микропроцессорах. Показана
  %эквивалентность этих ограничений определениям стратегий
  %вытеснения. Метод может быть эффективно использован в случае
  %тестовых шаблонов произвольного размера. В диссертации приведены
  %некоторые классы тестовых шаблонов, для которых генерируемые
  %ограничения имеют меньший размер, причем практика показывает, что
  %для определения многих ошибок достаточно тестовых шаблонов из таких
  %классов.
%\end{itemize}
